import nltk
import translator
from utility import *
import string
import re

def insert_fol(db, fol):
    fol = fol.strip()
    cmd = "INSERT INTO fol(formula) VALUES ('{}')".format(fol)
    result = execute(db, cmd)
    return "added {} fact(s): {}".format(result, fol)

def execute(db, cmd):
    result = db.cursor().execute(cmd)
    db.commit()
    return result

def answer_yesno_question(question, db):
    lp = nltk.LogicParser()
    facts = [lp.parse(x) for x in get_all_facts(db)]
    prover = nltk.Prover9()
    q = lp.parse(question)
    print "Question:", q
    result = prover.prove(q, facts)
    return result

def get_all_facts(db):
    cmd = "SELECT formula FROM fol"
    c = db.cursor()
    c.execute(cmd)
    facts = []
    for fact in c.fetchall():
        facts.append(fact[0])
    return facts

def answer_question(question, db):
    lp = nltk.LogicParser()
    facts = [lp.parse(x) for x in get_all_facts(db)]
#    print facts
    mc = nltk.MaceCommand(None, facts)
    mc.build_model()
    val = mc.valuation
#    print val
    dom = val.domain
    model = nltk.Model(dom, val)
    ass = nltk.Assignment(dom)
    q = lp.parse(question)
    print "Question:", q
    if len(q.free()) != 1:
        print "Question can only have one free variable"
        raise Exception()
    sat = model.satisfiers(q, q.free().pop().name, ass)
    answer = {}
    for obj in sat:
        answer[obj] = []
        for name, value in val.viewitems():
            if value == obj:
               multimap_add(answer, obj, name)
    return beautify2(answer)

def beautify2(m):
    result = []
    for e, syms in m.viewitems():
        names = []
        for n in syms:
            if not re.match('C\d*', n):
                names.append(n)
        if len(names) == 0:
            name = "Unnamed"
        else:
            name = names[0]
            if len(names) > 1:
                name += "(alias:{})".format(string.join(names[1:], ','))
        result.append(name)
    result = string.join(result, ', ')
    if result == '':
        result = 'None'
    return result
    
def beautify(m):
    result = ""
    for e, names in m.viewitems():
        result += "(identity {} with names {}) ".format(e, string.join(names, ", "))
    return result

def multimap_add(m, k ,v):
    m[k] = m.get(k, []) + [v]

def process_sentence(sentence, db):
    sentence = sentence.strip()
    if sentence == "":
        result = ""
    elif start_with(sentence, "f:"):
        fol = sentence[2:]
        result = insert_fol(db, fol.strip())
    elif start_with(sentence, "q:"):
        question = sentence[2:]
        result = answer_question(question, db)
    elif start_with(sentence, "qy:"):
        question = sentence[3:]
        result = answer_yesno_question(question, db)
    elif start_with(sentence, "cmd:"):
        cmd = sentence[4:]
        result = execute(db, cmd)
    else:
        fol, sen_type = translator.translate(sentence)
        if sen_type == "whq":
            result = answer_question(fol, db)
        elif sen_type == "ynq":
            result = answer_yesno_question(fol, db)
        elif sen_type == "fact":
            result = insert_fol(db, fol)
        else:
            result = "Unrecognized sentence type: "+sen_type

    return result
